minus2(x, y) -> cond3(ge2(x, s1(y)), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
ge2(u, 0) -> true
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(x0, 0)
minus2(x0, x1)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
cond3(true, x0, x1)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
minus2(x, y) -> cond3(ge2(x, s1(y)), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
ge2(u, 0) -> true
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(x0, 0)
minus2(x0, x1)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
cond3(true, x0, x1)
cond3(false, x0, x1)
MINUS2(x, y) -> COND3(ge2(x, s1(y)), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> GE2(x, s1(y))
GE2(s1(u), s1(v)) -> GE2(u, v)
minus2(x, y) -> cond3(ge2(x, s1(y)), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
ge2(u, 0) -> true
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(x0, 0)
minus2(x0, x1)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
cond3(true, x0, x1)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MINUS2(x, y) -> COND3(ge2(x, s1(y)), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(x, y) -> GE2(x, s1(y))
GE2(s1(u), s1(v)) -> GE2(u, v)
minus2(x, y) -> cond3(ge2(x, s1(y)), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
ge2(u, 0) -> true
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(x0, 0)
minus2(x0, x1)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
cond3(true, x0, x1)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
GE2(s1(u), s1(v)) -> GE2(u, v)
minus2(x, y) -> cond3(ge2(x, s1(y)), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
ge2(u, 0) -> true
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(x0, 0)
minus2(x0, x1)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
cond3(true, x0, x1)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
GE2(s1(u), s1(v)) -> GE2(u, v)
ge2(x0, 0)
minus2(x0, x1)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
cond3(true, x0, x1)
cond3(false, x0, x1)
ge2(x0, 0)
minus2(x0, x1)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
cond3(true, x0, x1)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
GE2(s1(u), s1(v)) -> GE2(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
MINUS2(x, y) -> COND3(ge2(x, s1(y)), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
minus2(x, y) -> cond3(ge2(x, s1(y)), x, y)
cond3(false, x, y) -> 0
cond3(true, x, y) -> s1(minus2(x, s1(y)))
ge2(u, 0) -> true
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(x0, 0)
minus2(x0, x1)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
cond3(true, x0, x1)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ UsableRulesProof
MINUS2(x, y) -> COND3(ge2(x, s1(y)), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(u, 0) -> true
ge2(x0, 0)
minus2(x0, x1)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
cond3(true, x0, x1)
cond3(false, x0, x1)
minus2(x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
MINUS2(x, y) -> COND3(ge2(x, s1(y)), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(u, 0) -> true
ge2(x0, 0)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
MINUS2(0, x0) -> COND3(false, 0, x0)
MINUS2(s1(x0), x1) -> COND3(ge2(x0, x1), s1(x0), x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
MINUS2(0, x0) -> COND3(false, 0, x0)
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(s1(x0), x1) -> COND3(ge2(x0, x1), s1(x0), x1)
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(u, 0) -> true
ge2(x0, 0)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ UsableRulesProof
COND3(true, x, y) -> MINUS2(x, s1(y))
MINUS2(s1(x0), x1) -> COND3(ge2(x0, x1), s1(x0), x1)
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(u, 0) -> true
ge2(x0, 0)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
MINUS2(s1(x0), s1(z1)) -> COND3(ge2(x0, s1(z1)), s1(x0), s1(z1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ UsableRulesProof
MINUS2(s1(x0), s1(z1)) -> COND3(ge2(x0, s1(z1)), s1(x0), s1(z1))
COND3(true, x, y) -> MINUS2(x, s1(y))
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(u, 0) -> true
ge2(x0, 0)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
COND3(true, s1(z0), s1(z1)) -> MINUS2(s1(z0), s1(s1(z1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
MINUS2(s1(x0), s1(z1)) -> COND3(ge2(x0, s1(z1)), s1(x0), s1(z1))
COND3(true, s1(z0), s1(z1)) -> MINUS2(s1(z0), s1(s1(z1)))
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(u, 0) -> true
ge2(x0, 0)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
MINUS2(x, y) -> COND3(ge2(x, s1(y)), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(u, 0) -> true
ge2(x0, 0)
minus2(x0, x1)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))
cond3(true, x0, x1)
cond3(false, x0, x1)
minus2(x0, x1)
cond3(true, x0, x1)
cond3(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
MINUS2(x, y) -> COND3(ge2(x, s1(y)), x, y)
COND3(true, x, y) -> MINUS2(x, s1(y))
ge2(0, s1(v)) -> false
ge2(s1(u), s1(v)) -> ge2(u, v)
ge2(u, 0) -> true
ge2(x0, 0)
ge2(0, s1(x0))
ge2(s1(x0), s1(x1))